E:Type, eq:EqDecider(E), prd:(E(E+Unit)), info:(E(IdId+(IdLnkE)Id)),
oax:EOrderAxioms(E; prd; info), T:(IdIdType), w, a:(x:Ide:ET(loc(e),x)),
sax:(e:E. first(e)  (x:Id. w(x,e) = a(x,pred(e))  T(loc(e),x))), V:(KndIdType),
v:(e:EV(kind(e),loc(e))).
mk-eval(E;eq;prd;info;oax;T;w;a;sax;V;v)  EventsWithValues 

latex

Definitions	pred(e), P & Q, A & B, Top, , mk-eval(E;eq;prd;info;oax;T;w;a;sax;V;v), EventsWithValues, kind(e), Knd, P  Q, A, b, first(e), Prop, loc(e), EOrderAxioms(E; pred?; info), Id, IdLnk, Unit, EqDecider(T), x:A. B(x), t  T
Lemmas	deq wf, unit wf, IdLnk wf, Id wf, EOrderAxioms wf, loc wf, first wf, assert wf, not wf, Knd wf, kind wf, it wf, top wf, pred wf, subtype rel self